Search for: All records

Abstract Spectre class of transient execution security attacks on modern microprocessors rely on speculative execution. Software Controlled Speculation (SCS) was proposed as a microarchitecture‐level defense in the original Spectre paper and has also been adopted by ARM. The idea with SCS is to allow a mode in the microarchitecture, where instructions that read from memory are not allowed to execute speculatively. Errors or malicious fault‐injections in the implementation of SCS can still render the microarchitecture vulnerable to Spectre attacks. A formal verification method is proposed that can check the correctness of the implementation of SCS and detect any faults. The method has been demonstrated to be very efficient on two sets of benchmarks and provides accurate detection of implementation faults in SCS. 

Abstract Transient execution attacks such as Spectre and Meltdown exploit speculative execution in modern microprocessors to leak information via cache side‐channels. Software solutions to defend against many transient execution attacks employ thelfenceserialising instruction, which does not allow instructions that come after thelfenceto execute out‐of‐order with respect to instructions that come before thelfence. However, errors and Trojans in the hardware implementation oflfencecan be exploited to compromise the software mitigations that uselfence. The aforementioned security gap has not been identified and addressed previously. The authors provide a formal method solution that addresses the verification oflfencehardware implementation. The authors also show how hardware Trojans can be designed to circumventlfenceand demonstrate that their verification approach will flag such Trojans as well. The authors have demonstrated the efficacy of our approach using RSD, which is an open source RISC‐V based superscalar out‐of‐order processor. 

Abstract With Cyber warfare, detection of hardware Trojans, malicious digital circuit components that can leak data and degrade performance, is an urgent issue. Quasi‐Delay Insensitive asynchronous digital circuits, such as NULL Convention Logic (NCL) and Sleep Convention Logic, also known as Multi‐Threshold NULL Convention Logic (MTNCL), have inherent security properties and resilience to large fluctuations in temperatures, which make them very alluring to extreme environment applications, such as space exploration, automotive, power industry etc. This paper shows how dual‐rail encoding used in NCL and MTNCL can be exploited to design Trojans, which would not be detected using existing methods. Generic threat models for Trojans are given. Formal verification methods that are capable of accurate detection of Trojans at the Register‐Transfer‐Level are also provided. The detection methods were tested by embedding Trojans in NCL and MTNCL Rivest‐Shamir‐Adleman (RSA) decryption circuits. The methods were applied to 25 NCL and 25 MTNCL RSA benchmarks of various data path width and provided 100% rate of detection.